$\forall$$p$:FinProbSpace, $f$:($\mathbb{N}\rightarrow\mathbb{N}$), $X$, $Y$:($n$:$\mathbb{N}\rightarrow$RandomVariable($p$;$f$($n$))).
\\[0ex]rv{-}iid($p$;$n$.$f$($n$);$n$.$X$($n$))
\\[0ex]$\Rightarrow$ rv{-}iid($p$;$n$.$f$($n$);$n$.$Y$($n$))
\\[0ex]$\Rightarrow$ ($\forall$$n$:$\mathbb{N}$, $i$:\{0..($n$+1)$^{-}$\}. rv{-}disjoint($p$;$f$($n$);$Y$($i$);$X$($n$)) \& rv{-}disjoint($p$;$f$($n$);$X$($i$);$Y$($n$)))
\\[0ex]$\Rightarrow$ rv{-}iid($p$;$n$.$f$($n$);$n$.$X$($n$) + $Y$($n$))